Nuprl Definition : unique_set
9,38
postcript
pdf
{!
x
:
T
|
P
(
x
)} == {
x
:
T
|
P
(
x
)
(
y
:
T
.
P
(
y
)
(
y
=
x
))}
latex
clarification:
{!
x
:
T
|
P
(
x
)} == {
x
:
T
|
P
(
x
)
(
y
:
T
.
P
(
y
)
(
y
=
x
T
))}
latex
Definitions
P
Q
,
x
:
A
.
B
(
x
)
,
P
Q
FDL editor aliases
unique_set
origin
(
y:T. P(y) 
(y = x))}
(y:T. P(y) (y = x 
T))} (y:T. P(y) (y = x))}
(y:T. P(y) (y = x T))} Qx:A. B(x) Q